Nuprl Lemma : b2i_bounds
9,38
postcript
pdf
b
:
. (0
b2i(
b
))
(b2i(
b
)
1)
latex
ProofTree
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
ff
,
False
,
P
Q
,
A
,
if
b
then
t
else
f
fi
,
tt
,
b2i(
b
)
,
A
B
,
P
Q
,
Unit
,
,
Lemmas
bool
wf
origin
b:
. (0 
b2i(b)) 
(b2i(b) 1)
b:. (0 b2i(b)) (b2i(b) 1)
Tx:A. B(x)
Q
A B Q